(* *)
Set Implicit Arguments.

Section SET_IMPL.
  
  Variable elem : Set.

  Definition set := elem -> Prop.

  Definition empty_set : set := fun e => False.

  Definition set_in (e: elem) (s: set) : Prop := s e.

  Definition set_intersect (s1: set) (s2: set) : set :=
    fun e => set_in e s1 /\ set_in e s2.

  Definition set_union (s1: set) (s2: set) : set :=
    fun e => set_in e s1 \/ set_in e s2.
  
  Definition set_complement (s: set) : set :=
    fun e => ~ set_in e s.
                          
  Definition set_subset (s1: set) (s2: set) : Prop :=
    forall e, set_in e s1 -> set_in e s2.

  Parameter set_length ()

End SET_IMPL.

Notation "e <- s" := (set_in e s)(at level 80).

Variable Individual : Set.

Variable Delta : set Individual.

Hypothesis Delta_includes_everything : 
  forall a : Individual, set_in a Delta.

Definition Class := set Individual.

Definition Top : Class := Delta.

Definition Bottom : Class := Delta.

Hypothesis Bottom_semantics: 
  forall a, 
    (a <- Bottom) -> False.

Variable Datatype : Set.

Definition ObjectProperty := Individual -> Individual -> Prop.

Definition DatatypeProperty := Individual -> Datatype -> Prop.

Definition someValuesFrom (op: ObjectProperty) (c: Class) : Class :=
  fun i => exists y, op i y /\ (y <- c).

Definition allValuesFrom (op: ObjectProperty) (c: Class) : Class :=
  fun i => forall y, op i y -> (y <- c).

Definition hasValue (op: ObjectProperty) : Class :=
  fun i => exists y, op i y.

Definition minCardinality (op: ObjectProperty) (n: nat) : Class :=
  fun i => exists y, op i y.






  
